Context-bounded analysis has been shown to be both efficient and effective atfinding bugs in concurrent programs. According to its original definition,context-bounded analysis explores all behaviors of a concurrent program up tosome fixed number of context switches between threads. This definition isinadequate for programs that create threads dynamically because bounding thenumber of context switches in a computation also bounds the number of threadsinvolved in the computation. In this paper, we propose a more generaldefinition of context-bounded analysis useful for programs with dynamic threadcreation. The idea is to bound the number of context switches for each threadinstead of bounding the number of switches of all threads. We consider severalvariants based on this new definition, and we establish decidability andcomplexity results for the analysis induced by them.
展开▼
